\begin{tabbing}
fifo+property(${\it es}$;${\it codes}$;${\it decodes}$;$C$;$S$;$R$;$T$;${\it Req}$;${\it Ack}$;$i$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=antecedent{-}surjection(${\it es}$;$\lambda$$e$.$R$($i$,$e$);$\lambda$$e$.$\exists$$j$:$C$. ($S$($j$,$i$,$e$));$f$)\+
\\[0ex]\& (\=$\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ $R$($i$,$e$)\} , $j$:\{$j$:$C$$\mid$ $S$($j$,$i$,$f$($e$))\} .\+
\\[0ex]${\it decodes}$($i$,$e$,es{-}state{-}when(${\it es}$;$e$)) = ${\it codes}$($j$,$i$,$f$($e$),es{-}state{-}when(${\it es}$;$f$($e$))) $\in$ $T$)
\-\\[0ex]\& (\=$\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ $R$($i$,$e$)\} , ${\it e'}$:\{$e$:es{-}E(${\it es}$)$\mid$ $R$($i$,$e$)\} , $j$:$C$.\+
\\[0ex]($S$($j$,$i$,$f$($e$))) $\Rightarrow$ ($S$($j$,$i$,$f$(${\it e'}$))) $\Rightarrow$ es{-}causle(${\it es}$;$f$($e$);$f$(${\it e'}$)) $\Rightarrow$ es{-}causle(${\it es}$;$e$;${\it e'}$))
\-\\[0ex]\& (\=$\forall$$j$:$C$.\+
\\[0ex]$\exists$\=${\it req}$:\{$e$:es{-}E(${\it es}$)$\mid$ ${\it Ack}$($j$,$i$,$e$)\} $\rightarrow$\{$e$:es{-}E(${\it es}$)$\mid$ $S$($j$,$i$,$e$) \& ${\it Req}$($j$,$e$)\} \+
\\[0ex](antecedent{-}surjection(${\it es}$;$\lambda$$e$.${\it Ack}$($j$,$i$,$e$);$\lambda$$e$.$S$($j$,$i$,$e$) \& ${\it Req}$($j$,$e$);${\it req}$)
\\[0ex]\& (\=$\forall$$a$:\{$e$:es{-}E(${\it es}$)$\mid$ ${\it Ack}$($j$,$i$,$e$)\} .\+
\\[0ex]$\exists$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ $R$($i$,$e$)\} . ($f$($e$) = ${\it req}$($a$) $\in$ es{-}E(${\it es}$) \& es{-}causle(${\it es}$;$e$;$a$)))
\-\\[0ex]\& causal{-}order{-}preserving(${\it es}$;$e$.${\it req}$($e$);$e$.${\it Ack}$($j$,$i$,$e$))))
\-\-\-
\end{tabbing}